(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 33))
(declare-fun v1 () (_ BitVec 83))
(declare-fun v2 () (_ BitVec 65))
(declare-fun v3 () (_ BitVec 82))
(assert (let ((e4(_ bv4951940282 34)))
(let ((e5 (ite (bvsge ((_ zero_extend 49) v0) v3) (_ bv1 1) (_ bv0 1))))
(let ((e6 (bvlshr e4 ((_ zero_extend 33) e5))))
(let ((e7 (ite (bvugt e6 e6) (_ bv1 1) (_ bv0 1))))
(let ((e8 (ite (bvule e6 e6) (_ bv1 1) (_ bv0 1))))
(let ((e9 (bvxnor v3 ((_ zero_extend 48) e6))))
(let ((e10 (ite (bvsge v2 ((_ sign_extend 64) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e11 (ite (bvule ((_ zero_extend 31) e6) v2) (_ bv1 1) (_ bv0 1))))
(let ((e12 (bvxor ((_ zero_extend 64) e10) v2)))
(let ((e13 ((_ repeat 62) e10)))
(let ((e14 (bvnot v0)))
(let ((e15 (bvxnor e9 ((_ zero_extend 17) v2))))
(let ((e16 (bvneg e9)))
(let ((e17 (ite (bvslt ((_ zero_extend 64) e5) v2) (_ bv1 1) (_ bv0 1))))
(let ((e18 ((_ rotate_left 0) e11)))
(let ((e19 ((_ repeat 1) e15)))
(let ((e20 (ite (distinct v3 ((_ zero_extend 81) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e21 ((_ extract 0 0) e20)))
(let ((e22 ((_ sign_extend 27) e12)))
(let ((e23 (ite (= ((_ zero_extend 64) e21) e12) (_ bv1 1) (_ bv0 1))))
(let ((e24 (ite (bvsge e10 e7) (_ bv1 1) (_ bv0 1))))
(let ((e25 (bvneg e8)))
(let ((e26 (bvnand e22 ((_ zero_extend 91) e10))))
(let ((e27 (bvsub ((_ zero_extend 81) e8) e16)))
(let ((e28 (bvshl e20 e5)))
(let ((e29 (bvurem ((_ zero_extend 81) e7) e15)))
(let ((e30 (bvor ((_ zero_extend 20) e13) e19)))
(let ((e31 (ite (bvslt e9 ((_ zero_extend 81) e10)) (_ bv1 1) (_ bv0 1))))
(let ((e32 (ite (bvugt e14 ((_ zero_extend 32) e25)) (_ bv1 1) (_ bv0 1))))
(let ((e33 (bvshl e13 ((_ zero_extend 29) v0))))
(let ((e34 (bvsrem ((_ zero_extend 81) e31) e30)))
(let ((e35 (bvnand e9 ((_ sign_extend 49) e14))))
(let ((e36 ((_ sign_extend 26) e11)))
(let ((e37 (bvneg v1)))
(let ((e38 (bvule ((_ zero_extend 91) e17) e22)))
(let ((e39 (= ((_ sign_extend 20) e33) e9)))
(let ((e40 (bvule ((_ zero_extend 81) e11) e16)))
(let ((e41 (bvuge e34 e15)))
(let ((e42 (bvuge e18 e10)))
(let ((e43 (bvule e30 ((_ zero_extend 81) e18))))
(let ((e44 (bvugt e27 ((_ zero_extend 81) e31))))
(let ((e45 (bvslt v3 e35)))
(let ((e46 (bvult e19 ((_ zero_extend 20) e33))))
(let ((e47 (distinct e36 ((_ sign_extend 26) e18))))
(let ((e48 (bvsle ((_ zero_extend 10) e29) e22)))
(let ((e49 (bvuge e19 ((_ sign_extend 49) e14))))
(let ((e50 (bvsle e19 ((_ zero_extend 81) e17))))
(let ((e51 (bvuge ((_ sign_extend 33) e21) e4)))
(let ((e52 (distinct e22 ((_ zero_extend 91) e32))))
(let ((e53 (bvsle e30 ((_ sign_extend 48) e6))))
(let ((e54 (bvuge e15 ((_ sign_extend 81) e31))))
(let ((e55 (bvule e34 ((_ zero_extend 81) e21))))
(let ((e56 (bvsgt ((_ sign_extend 35) e36) e33)))
(let ((e57 (bvuge ((_ sign_extend 81) e8) e19)))
(let ((e58 (bvugt ((_ zero_extend 64) e32) v2)))
(let ((e59 (bvule ((_ zero_extend 17) e12) e27)))
(let ((e60 (bvsge e30 ((_ zero_extend 81) e18))))
(let ((e61 (bvsle e19 ((_ sign_extend 48) e6))))
(let ((e62 (bvslt ((_ sign_extend 81) e5) e29)))
(let ((e63 (bvuge ((_ sign_extend 1) e15) e37)))
(let ((e64 (bvule ((_ sign_extend 1) e14) e6)))
(let ((e65 (bvule e22 ((_ sign_extend 27) e12))))
(let ((e66 (= e12 ((_ sign_extend 32) v0))))
(let ((e67 (bvsge e9 ((_ zero_extend 20) e33))))
(let ((e68 (bvsge v2 ((_ sign_extend 64) e5))))
(let ((e69 (bvuge ((_ zero_extend 81) e17) e30)))
(let ((e70 (bvugt ((_ sign_extend 61) e21) e13)))
(let ((e71 (bvslt e33 ((_ zero_extend 61) e17))))
(let ((e72 (bvsle e5 e28)))
(let ((e73 (= e37 ((_ sign_extend 56) e36))))
(let ((e74 (bvsgt e19 e35)))
(let ((e75 (bvugt e19 ((_ sign_extend 81) e20))))
(let ((e76 (bvuge e15 ((_ zero_extend 55) e36))))
(let ((e77 (= ((_ zero_extend 33) e17) e6)))
(let ((e78 (bvslt e27 ((_ sign_extend 81) e5))))
(let ((e79 (bvult e14 ((_ zero_extend 32) e23))))
(let ((e80 (bvsle v2 ((_ zero_extend 64) e11))))
(let ((e81 (bvugt e29 e9)))
(let ((e82 (= e16 e27)))
(let ((e83 (bvsgt ((_ zero_extend 91) e32) e22)))
(let ((e84 (bvsge ((_ zero_extend 81) e24) e16)))
(let ((e85 (= ((_ sign_extend 81) e10) e16)))
(let ((e86 (bvsge ((_ sign_extend 81) e7) v3)))
(let ((e87 (bvult e12 ((_ zero_extend 3) e13))))
(let ((e88 (bvsle v3 e30)))
(let ((e89 (bvsgt e9 ((_ zero_extend 81) e24))))
(let ((e90 (bvugt e14 e14)))
(let ((e91 (bvugt ((_ sign_extend 61) e21) e33)))
(let ((e92 (bvult e36 ((_ sign_extend 26) e8))))
(let ((e93 (= e19 ((_ sign_extend 49) v0))))
(let ((e94 (bvult e30 ((_ sign_extend 81) e21))))
(let ((e95 (bvslt e26 ((_ zero_extend 91) e18))))
(let ((e96 (distinct e37 ((_ sign_extend 1) e35))))
(let ((e97 (distinct ((_ sign_extend 91) e17) e26)))
(let ((e98 (bvsge ((_ sign_extend 55) e36) e16)))
(let ((e99 (bvsge ((_ zero_extend 49) e14) e30)))
(let ((e100 (bvsgt e18 e32)))
(let ((e101 (bvugt ((_ zero_extend 81) e20) v3)))
(let ((e102 (bvult ((_ sign_extend 61) e32) e13)))
(let ((e103 (bvule e18 e5)))
(let ((e104 (bvsgt v1 ((_ zero_extend 56) e36))))
(let ((e105 (bvugt e28 e21)))
(let ((e106 (bvule e8 e8)))
(let ((e107 (= e27 ((_ sign_extend 48) e4))))
(let ((e108 (bvult v1 ((_ sign_extend 82) e31))))
(let ((e109 (bvsge ((_ sign_extend 81) e31) e34)))
(let ((e110 (distinct ((_ sign_extend 64) e10) e12)))
(let ((e111 (bvsgt e31 e25)))
(let ((e112 (ite e77 e41 e85)))
(let ((e113 (not e67)))
(let ((e114 (and e45 e50)))
(let ((e115 (not e75)))
(let ((e116 (= e38 e47)))
(let ((e117 (or e89 e80)))
(let ((e118 (= e72 e99)))
(let ((e119 (and e108 e118)))
(let ((e120 (=> e102 e119)))
(let ((e121 (=> e91 e44)))
(let ((e122 (xor e121 e87)))
(let ((e123 (= e83 e64)))
(let ((e124 (=> e113 e111)))
(let ((e125 (= e71 e40)))
(let ((e126 (and e109 e62)))
(let ((e127 (xor e55 e46)))
(let ((e128 (xor e78 e39)))
(let ((e129 (and e93 e117)))
(let ((e130 (or e60 e49)))
(let ((e131 (and e127 e128)))
(let ((e132 (and e104 e98)))
(let ((e133 (and e107 e53)))
(let ((e134 (xor e57 e65)))
(let ((e135 (=> e54 e122)))
(let ((e136 (or e63 e120)))
(let ((e137 (=> e81 e58)))
(let ((e138 (=> e73 e110)))
(let ((e139 (=> e114 e92)))
(let ((e140 (and e86 e100)))
(let ((e141 (and e103 e105)))
(let ((e142 (not e116)))
(let ((e143 (and e133 e132)))
(let ((e144 (=> e61 e112)))
(let ((e145 (or e95 e70)))
(let ((e146 (=> e76 e134)))
(let ((e147 (=> e124 e79)))
(let ((e148 (xor e74 e147)))
(let ((e149 (= e90 e136)))
(let ((e150 (=> e123 e135)))
(let ((e151 (not e68)))
(let ((e152 (=> e43 e142)))
(let ((e153 (xor e97 e59)))
(let ((e154 (or e101 e140)))
(let ((e155 (=> e143 e139)))
(let ((e156 (xor e141 e126)))
(let ((e157 (or e149 e82)))
(let ((e158 (or e115 e48)))
(let ((e159 (ite e88 e84 e69)))
(let ((e160 (= e52 e66)))
(let ((e161 (ite e130 e42 e154)))
(let ((e162 (and e150 e131)))
(let ((e163 (= e125 e152)))
(let ((e164 (=> e144 e160)))
(let ((e165 (= e161 e106)))
(let ((e166 (and e138 e137)))
(let ((e167 (not e94)))
(let ((e168 (or e96 e146)))
(let ((e169 (=> e162 e165)))
(let ((e170 (ite e159 e145 e153)))
(let ((e171 (= e158 e129)))
(let ((e172 (and e163 e171)))
(let ((e173 (xor e172 e151)))
(let ((e174 (= e157 e169)))
(let ((e175 (= e174 e148)))
(let ((e176 (ite e156 e170 e167)))
(let ((e177 (not e175)))
(let ((e178 (= e51 e176)))
(let ((e179 (or e155 e177)))
(let ((e180 (and e56 e179)))
(let ((e181 (and e168 e173)))
(let ((e182 (or e166 e181)))
(let ((e183 (or e178 e164)))
(let ((e184 (ite e182 e182 e182)))
(let ((e185 (or e183 e180)))
(let ((e186 (not e185)))
(let ((e187 (and e184 e186)))
(let ((e188 (and e187 (not (= e15 (_ bv0 82))))))
(let ((e189 (and e188 (not (= e30 (_ bv0 82))))))
(let ((e190 (and e189 (not (= e30 (bvnot (_ bv0 82)))))))
e190
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
